プログラム検証入門(2) 自動検証はなぜ困難が，プログラム意味論とは